$\forall$$B$:Type, $k$:Knd, $f$:(Id$\rightarrow$$B$), $g$:(IdLnk$\rightarrow$Id$\rightarrow$$B$). kindcase($k$; $a$.$f$($a$); $l$,$t$.$g$($l$,$t$)) $\in$ $B$